Generate function bodies with nondet return values #3457

danpoe · 2018-11-24T13:09:01Z

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

smowton

Cursory review because this is big. For a more thorough look over I recommend introducing this in stages

smowton · 2018-11-26T09:10:17Z

src/langapi/language.h

@@ -70,8 +70,7 @@ class languaget:public messaget
  /// complete. Functions introduced here are visible to lazy loading and
  /// can influence its decisions (e.g. picking the types of input parameters
  /// and globals), whereas anything introduced during `final` cannot.
-  virtual bool generate_support_functions(
-    symbol_tablet &symbol_table)=0;
+  virtual bool generate_support_functions(symbol_tablet &symbol_table) = 0;


Unrelated restyle in commit

smowton · 2018-11-26T09:10:38Z

src/langapi/language_file.cpp

@@ -10,6 +10,8 @@ Author: Daniel Kroening, [email protected]

 #include <fstream>

+#include <util/object_factory_parameters.h>


Adding an include but nothing that uses it (in this commit)?

smowton · 2018-11-26T09:11:32Z

src/ansi-c/c_nondet_symbol_factory.cpp

-/// \param loc: The location to assign to the symbol
-/// \param type: The type of symbol to create
-/// \param static_lifetime: Whether the symbol should have a static lifetime
-/// \param prefix: The prefix to use for the symbol's basename


Why is this in this PR?

smowton · 2018-11-26T09:13:20Z

regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/main.c

+  assert(p->prev != &dummy);
+
+  assert(p->next != NULL);
+  assert(p->next != &dummy);


Also assert p->next != p->prev?

smowton · 2018-11-26T09:14:46Z

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -181,7 +224,6 @@ void symbol_factoryt::gen_nondet_init(
 /// \param base_name: The name to use for the symbol created
 /// \param type: The type for the symbol created
 /// \param loc: The location to assign to generated code
-/// \param allow_null: Whether to allow a null value when type is a pointer


does removing this unused parameter belong in a different commit?

smowton · 2018-11-26T09:16:06Z

src/util/allocate_objects.cpp

+exprt allocate_objectst::allocate_object(
+  code_blockt &assignments,
+  const exprt &target_expr,
+  const typet &allocate_type,


allocate_type and alloc_type are very similar names

smowton · 2018-11-26T09:17:51Z

src/util/allocate_objects.h

+  GLOBAL,
+  /// Allocate local stacked objects
+  LOCAL,
+  /// Allocate dynamic objects (using MALLOC)


now using ALLOCATE

danpoe · 2018-11-26T11:01:56Z

@smowton Thanks for the review! The PR is based on another open PR (#3455) and in this one only the last two commits are new (see PR description).

kroening · 2018-11-28T20:25:36Z

Should this live in goto-instrument? It's an instrumentation.

kroening

Should be in goto-instrument!

danpoe · 2018-11-29T13:58:00Z

@kroening One thing this PR does is move generate_function_bodies.h/cpp from goto-programs to goto-instrument. However I left the C object factory in ansi-c (just like the Java object factory is in java_bytecode). Are you suggesting to move the C object factory to goto-instrument as well?

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: f2506f9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/93055935

…-targets Generate function bodies that nondet havoc the function arguments [blocks: #3457]

danpoe · 2019-01-22T15:01:32Z

@kroening This is now done in goto-instrument.

chrisr-diffblue

LGTM

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: cc4baa5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98196114
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

Extends the generate function bodies feature to create nondet return values for functions, using the c nondet symbol factory.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 5fa9452).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98301475

danpoe requested review from cesaro, chrisr-diffblue, cristina-david, kroening, martin-cs, NathanJPhillips, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners November 24, 2018 13:09

tautschnig assigned danpoe Nov 24, 2018

smowton reviewed Nov 26, 2018

View reviewed changes

danpoe force-pushed the feature/nondet-return-values branch from 3dbd888 to 9a2abb1 Compare November 27, 2018 15:59

kroening requested changes Nov 28, 2018

View reviewed changes

danpoe added the dependent - do not merge label Nov 29, 2018

danpoe changed the title ~~Generate function bodies with nondet return values~~ Generate function bodies with nondet return values [depends-on: #3455] Nov 29, 2018

danpoe force-pushed the feature/nondet-return-values branch from 9a2abb1 to f2506f9 Compare November 29, 2018 17:52

allredj reviewed Nov 29, 2018

View reviewed changes

danpoe force-pushed the feature/nondet-return-values branch from f2506f9 to 923a9eb Compare December 19, 2018 11:49

danpoe added a commit that referenced this pull request Jan 22, 2019

Merge pull request #3455 from danpoe/feature/nondet-function-argument…

81d8eb1

…-targets Generate function bodies that nondet havoc the function arguments [blocks: #3457]

danpoe force-pushed the feature/nondet-return-values branch from 923a9eb to 27d3a72 Compare January 22, 2019 14:45

danpoe removed the dependent - do not merge label Jan 22, 2019

danpoe changed the title ~~Generate function bodies with nondet return values [depends-on: #3455]~~ Generate function bodies with nondet return values Jan 22, 2019

danpoe removed their assignment Jan 22, 2019

danpoe force-pushed the feature/nondet-return-values branch from 27d3a72 to cc4baa5 Compare January 22, 2019 15:00

danpoe assigned kroening Jan 22, 2019

chrisr-diffblue approved these changes Jan 22, 2019

View reviewed changes

allredj reviewed Jan 22, 2019

View reviewed changes

kroening approved these changes Jan 22, 2019

View reviewed changes

kroening assigned danpoe and unassigned kroening Jan 22, 2019

danpoe force-pushed the feature/nondet-return-values branch from cc4baa5 to 5fa9452 Compare January 23, 2019 10:39

danpoe added 2 commits January 23, 2019 10:39

Generate function bodies with nondet return values

20c4bc1

Extends the generate function bodies feature to create nondet return values for functions, using the c nondet symbol factory.

Add regression tests for nondet return value generation

5fa9452

allredj reviewed Jan 23, 2019

View reviewed changes

danpoe merged commit 9f1f3f5 into diffblue:develop Jan 23, 2019

danpoe deleted the feature/nondet-return-values branch June 2, 2020 17:20

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Generate function bodies with nondet return values #3457

Generate function bodies with nondet return values #3457

danpoe commented Nov 24, 2018 •

edited

Loading

smowton left a comment

smowton Nov 26, 2018

smowton Nov 26, 2018

smowton Nov 26, 2018

smowton Nov 26, 2018

smowton Nov 26, 2018

smowton Nov 26, 2018

smowton Nov 26, 2018

danpoe commented Nov 26, 2018

kroening commented Nov 28, 2018

kroening left a comment

danpoe commented Nov 29, 2018

allredj left a comment

danpoe commented Jan 22, 2019

chrisr-diffblue left a comment

allredj left a comment

allredj left a comment

		@@ -10,6 +10,8 @@ Author: Daniel Kroening, [email protected]

		#include <fstream>

		#include <util/object_factory_parameters.h>

Generate function bodies with nondet return values #3457

Generate function bodies with nondet return values #3457

Conversation

danpoe commented Nov 24, 2018 • edited Loading

smowton left a comment

Choose a reason for hiding this comment

smowton Nov 26, 2018

Choose a reason for hiding this comment

smowton Nov 26, 2018

Choose a reason for hiding this comment

smowton Nov 26, 2018

Choose a reason for hiding this comment

smowton Nov 26, 2018

Choose a reason for hiding this comment

smowton Nov 26, 2018

Choose a reason for hiding this comment

smowton Nov 26, 2018

Choose a reason for hiding this comment

smowton Nov 26, 2018

Choose a reason for hiding this comment

danpoe commented Nov 26, 2018

kroening commented Nov 28, 2018

kroening left a comment

Choose a reason for hiding this comment

danpoe commented Nov 29, 2018

allredj left a comment

Choose a reason for hiding this comment

danpoe commented Jan 22, 2019

chrisr-diffblue left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

danpoe commented Nov 24, 2018 •

edited

Loading